| Definitions | ES, (x  l), AbsInterface(A), x:A  B(x),  x:A. B(x), E(X), P   Q, f**(e), {x:A| B(x)} , prior-f-fixedpoints(e), [car / cdr], left + right, P  Q, P  Q, x:A  B(x), P & Q, P Q, s = t, hd(l), last(L), l[i],  b, (e < e'), e c e', Top, f(a), Type, t T,  , <a, b>,  , True,  T, type List, EState(T), a:A fp B(a), Id,  , strong-subtype(A;B), EqDecider(T), Unit, IdLnk, EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M),  , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r s, e < e', constant_function(f;A;B), SWellFounded(R(x;y)), pred!(e;e'),   x,y. t(x;y), Void,  x:A.B(x), S  T, suptype(S; T), first(e),  A, pred(e), x.A(x), x. t(x), E, e  X, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , ff, b, tt, let x,y = A in B(x;y), False, p q, p  q, p q, {T}, SQType(T), s ~ t, e = e', [], as @ bs, X(e),  , Outcome, #$n, A B, a < b, ||as||, |g|, A c B, A List , p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, x f y, a < b, [d], eq_atom$n(x;y), q_le(r;s), q_less(a;b), qeq(r;s), a = b, a = b, deq-member(eq;x;L), prior(X), y is f*(x),  x:A. B(x), y=f*(x) via L |
| Lemmas | es-fix property, member append, length wf1, select wf, es-interface-val wf2, es-prior-fixedpoints wf, es-prior-interface wf, es-interface-val wf, member singleton, bool cases, guard wf, bool sq, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-es-eq-E-2, es-eq-E wf, bnot wf, false wf, strong-subtype wf, strong-subtype-self, es-interface wf, es-is-interface wf, es-causl wf, es-causle wf, es-E-interface-subtype rel, es-E wf, deq wf, EOrderAxioms wf, kind wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, Knd wf, kindcase wf, IdLnk wf, constant function wf, loc wf, not wf, assert wf, first wf, top wf, unit wf, pred! wf, strongwellfounded wf, member wf, rationals wf, Id wf, EState wf, subtype rel wf, event system wf, iff wf, rev implies wf, l member wf, squash wf, true wf, es-prior-fixedpoints-fix, es-fix wf2, es-fix wf, es-E-interface wf, l member subtype |